COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE INDVAR r,PREDPAR A 2 B 1
C00004 00003	% Definitions %
C00005 ENDMK
C⊗;
DECLARE INDVAR r,PREDPAR A 2 B 1;

AXIOM ZF:
% Extensionality %  
EXT: 	∀x y.isset(x)∧isset(y) ⊃ (∀z.(zεx≡zεy)≡x=y));

% Null set %
EMT: 	∀x.¬xεNIL;

% Unordered pair %
PAIR: 	∀x y w.(wε{x,y}≡w=x∨w=y);

% Sum set %
UNION: 	∀x z.(zεunion(x)≡∃t.(zεt∧tεx));

% Infinity %
INF: 	(0εInf∧∀y.(yεInf⊃(y∪{y})εInf));

% Replacement is equivalent to
∀x.∃!y.A(x,y) ⊃ ∀u.∃v.∀r.(rεv ≡ ∃s.(sεu∧A(s,r))) % 

REPL:	∀x.(∃y.A(x,y)∧∀y z.(A(x,y)∧A(x,z)⊃y=z)) ⊃
	∀u.∃v.(∀r.(rεv ≡ ∃s.(sεu∧A(s,r))))  ;

% Separation(weaker than replacment) %
SEP:	∀x.∃y.∀z.(zεy≡zεx∧B(z));

% Power set %
POWER:	∀x z.(zεpower(x)≡z⊂x);

% Regularity %
REG:	∀x.∃y.(x=0∨(yεx∧∀z.(zεx⊃¬zεy))); ; ;

% Definitions %

DECLARE PREDCONST FUN 1 INTO 2 PSUBSET 2,
	OPCONST rng 1 dom 1;

AXIOM
SUBSET:		∀x y.(x⊂y≡∀z.(zεx⊃zεy));
PROPSUBSET:	∀x y.(PSUBSET(x,y)≡x⊂y∧¬x=y);
PAIRFUN:     	∀x y z.(zε{x,y}≡z=x∨z=y);
UNITSETFUN:	∀x.( {x}={x,x} );
OPAIRFUN:	∀x y.( <x,y>={{x},{x,y}} );
FUNCTION:	∀w.(FUN(w)≡∀z.(zεw⊃∃x y.(z=<x,y>))∧
			   ∀x y z.(<x,y>εw∧<x,z>εw⊃y=z) );
DOMAIN:		∀w x.(xεdom(w)≡FUN(w)∧∃y z.(yεw∧y=<x,z>));
RANGE:		∀w x.(xεrng(w)≡FUN(w)∧∃y z.(yεw∧y=<z,x>));
INTO:           ∀w x.(INTO(w,x)≡x⊂rng(w));
UNION:		∀x y z.(zεx∪y≡zεx∨zεy); ;